| Definitions | s = t, t  T, x:A  B(x),  x:A. B(x), ES, EState(T), a:A fp B(a), f(a), Id,  , strong-subtype(A;B), P   Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e',  ,  b, constant_function(f;A;B), SWellFounded(R(x;y)),  , pred!(e;e'),   x,y. t(x;y), Void,  x:A.B(x), Top, S  T, suptype(S; T), first(e),  A, <a, b>, pred(e), x.A(x), x. t(x), P & Q, chain_master(), E, chain_config(), AbsInterface(A), chain_sys(Cmd), e  X, P  Q, {x:A| B(x)} , E(X), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , X(e), csupdate?(x), tt, inr x , "$token", ff, inl x , Atom, False, True, master-constraints(es;Master),  x:A. B(x), update-antecedent{i:l}(es;Cmd;Sys;Config;u), (e <loc e'),  , |g|, cmseq-num(x), cmd-history(e), ||as||, cmseq-from(x), loc(e), cmseq-to(x), ccpred-id(x), ccpred?(x), let x = a in b(x), (e < e'), cmseq?(x), L1 L2, e c e', hd(l), config-antecedent(es;Master;Config;c), master-antecedent{i:l}(es;Cmd;Master;Config;Sys;m), a < b, chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), valid-sys(es;Config;Sys;e), A B, ccsucc?(x), nth_tl(n;as), csupdate-cmds(x), ccsucc-num(x), ccsucc-id(x), sys-cmds(x), A c B, cmconfig-list(x), i j < k, n - m, -n, n+m, {i..j }, #$n, i  j , l[i], Outcome, last(L), null(as), cmconfig?(x), chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num)), chain-replication{i:l}(es;Cmd;Sys;Config;Master;u) |
| Lemmas | es-causle wf, sublist wf, master-constraints wf, config-antecedent wf, chain config ind wf, cmconfig? wf, ge wf, hd wf, null wf3, last wf, int seg wf, select wf, le wf, cmconfig-list wf, update-antecedent wf, sys-cmds wf, ccsucc-id wf, ccsucc-num wf, csupdate-cmds wf, nth tl wf, valid-sys wf, ccsucc? wf, master-antecedent wf, cmseq? wf, es-locl wf, es-causl wf, let wf, ccpred? wf, ccpred-id wf, cmseq-to wf, es-loc wf, cmseq-from wf, length wf1, cmd-history wf, cmseq-num wf, es-interface-val wf, csupdate? wf, es-interface-val wf2, true wf, false wf, es-interface wf, es-E-interface wf, bfalse wf, btrue wf, es-is-interface wf, chain sys wf, chain config wf, es-E wf, chain master wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf |
Sys:AbsInterface(chain_sys(Cmd)),